Problem:
top(sent(x)) -> top(check(rest(x)))
rest(nil()) -> sent(nil())
rest(cons(x,y)) -> sent(y)
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
check(cons(x,y)) -> cons(x,y)
Proof:
Complexity Transformation Processor:
strict:
top(sent(x)) -> top(check(rest(x)))
rest(nil()) -> sent(nil())
rest(cons(x,y)) -> sent(y)
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
check(cons(x,y)) -> cons(x,y)
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[cons](x0, x1) = x0 + x1,
[nil] = 0,
[check](x0) = x0 + 9,
[rest](x0) = x0,
[top](x0) = x0 + 127,
[sent](x0) = x0
orientation:
top(sent(x)) = x + 127 >= x + 136 = top(check(rest(x)))
rest(nil()) = 0 >= 0 = sent(nil())
rest(cons(x,y)) = x + y >= y = sent(y)
check(sent(x)) = x + 9 >= x + 9 = sent(check(x))
check(rest(x)) = x + 9 >= x + 9 = rest(check(x))
check(cons(x,y)) = x + y + 9 >= x + y + 9 = cons(check(x),y)
check(cons(x,y)) = x + y + 9 >= x + y + 9 = cons(x,check(y))
check(cons(x,y)) = x + y + 9 >= x + y = cons(x,y)
problem:
strict:
top(sent(x)) -> top(check(rest(x)))
rest(nil()) -> sent(nil())
rest(cons(x,y)) -> sent(y)
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
weak:
check(cons(x,y)) -> cons(x,y)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[cons](x0, x1) = x0 + x1,
[nil] = 0,
[check](x0) = x0,
[rest](x0) = x0,
[top](x0) = x0 + 6,
[sent](x0) = x0 + 2
orientation:
top(sent(x)) = x + 8 >= x + 6 = top(check(rest(x)))
rest(nil()) = 0 >= 2 = sent(nil())
rest(cons(x,y)) = x + y >= y + 2 = sent(y)
check(sent(x)) = x + 2 >= x + 2 = sent(check(x))
check(rest(x)) = x >= x = rest(check(x))
check(cons(x,y)) = x + y >= x + y = cons(check(x),y)
check(cons(x,y)) = x + y >= x + y = cons(x,check(y))
check(cons(x,y)) = x + y >= x + y = cons(x,y)
problem:
strict:
rest(nil()) -> sent(nil())
rest(cons(x,y)) -> sent(y)
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
weak:
top(sent(x)) -> top(check(rest(x)))
check(cons(x,y)) -> cons(x,y)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[cons](x0, x1) = x0 + x1 + 6,
[nil] = 0,
[check](x0) = x0,
[rest](x0) = x0,
[top](x0) = x0 + 8,
[sent](x0) = x0 + 4
orientation:
rest(nil()) = 0 >= 4 = sent(nil())
rest(cons(x,y)) = x + y + 6 >= y + 4 = sent(y)
check(sent(x)) = x + 4 >= x + 4 = sent(check(x))
check(rest(x)) = x >= x = rest(check(x))
check(cons(x,y)) = x + y + 6 >= x + y + 6 = cons(check(x),y)
check(cons(x,y)) = x + y + 6 >= x + y + 6 = cons(x,check(y))
top(sent(x)) = x + 12 >= x + 8 = top(check(rest(x)))
check(cons(x,y)) = x + y + 6 >= x + y + 6 = cons(x,y)
problem:
strict:
rest(nil()) -> sent(nil())
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
weak:
rest(cons(x,y)) -> sent(y)
top(sent(x)) -> top(check(rest(x)))
check(cons(x,y)) -> cons(x,y)
Splitting Processor:
strict:
check(cons(x,y)) -> cons(x,check(y))
weak:
rest(cons(x,y)) -> sent(y)
top(sent(x)) -> top(check(rest(x)))
check(cons(x,y)) -> cons(x,y)
rest(nil()) -> sent(nil())
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
check(cons(x,y)) -> cons(check(x),y)
Matrix Interpretation Processor:
dimension: 4
max_matrix:
[1 1 1 1]
[0 1 0 0]
[0 0 0 0]
[0 0 0 0]
interpretation:
[1 0 0 1] [1 1 1 0] [1]
[0 1 0 0] [0 1 0 0] [1]
[cons](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0]
[0 0 0 0] [0 0 0 0] [0],
[0]
[0]
[nil] = [0]
[0],
[1 1 0 0]
[0 1 0 0]
[check](x0) = [0 0 0 0]x0
[0 0 0 0] ,
[1 0 0 0]
[0 1 0 0]
[rest](x0) = [0 0 0 0]x0
[0 0 0 0] ,
[1 1 0 0] [0]
[0 0 0 0] [0]
[top](x0) = [0 0 0 0]x0 + [0]
[0 0 0 0] [1],
[1 1 1 0]
[0 1 0 0]
[sent](x0) = [0 0 0 0]x0
[0 0 0 0]
orientation:
[0] [0]
[0] [0]
rest(nil()) = [0] >= [0] = sent(nil())
[0] [0]
[1 2 1 0] [1 2 0 0]
[0 1 0 0] [0 1 0 0]
check(sent(x)) = [0 0 0 0]x >= [0 0 0 0]x = sent(check(x))
[0 0 0 0] [0 0 0 0]
[1 1 0 0] [1 1 0 0]
[0 1 0 0] [0 1 0 0]
check(rest(x)) = [0 0 0 0]x >= [0 0 0 0]x = rest(check(x))
[0 0 0 0] [0 0 0 0]
[1 1 0 1] [1 2 1 0] [2] [1 1 0 0] [1 1 1 0] [1]
[0 1 0 0] [0 1 0 0] [1] [0 1 0 0] [0 1 0 0] [1]
check(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = cons(check(x),y)
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0]
[1 1 0 1] [1 2 1 0] [2] [1 0 0 1] [1 2 0 0] [1]
[0 1 0 0] [0 1 0 0] [1] [0 1 0 0] [0 1 0 0] [1]
check(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = cons(x,check(y))
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0]
[1 0 0 1] [1 1 1 0] [1] [1 1 1 0]
[0 1 0 0] [0 1 0 0] [1] [0 1 0 0]
rest(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]y = sent(y)
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0]
[1 2 1 0] [0] [1 2 0 0] [0]
[0 0 0 0] [0] [0 0 0 0] [0]
top(sent(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = top(check(rest(x)))
[0 0 0 0] [1] [0 0 0 0] [1]
[1 1 0 1] [1 2 1 0] [2] [1 0 0 1] [1 1 1 0] [1]
[0 1 0 0] [0 1 0 0] [1] [0 1 0 0] [0 1 0 0] [1]
check(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = cons(x,y)
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0]
problem:
strict:
rest(nil()) -> sent(nil())
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
weak:
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
rest(cons(x,y)) -> sent(y)
top(sent(x)) -> top(check(rest(x)))
check(cons(x,y)) -> cons(x,y)
Splitting Processor:
strict:
rest(nil()) -> sent(nil())
weak:
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
rest(cons(x,y)) -> sent(y)
top(sent(x)) -> top(check(rest(x)))
check(cons(x,y)) -> cons(x,y)
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
Splitting Processor:
strict:
check(sent(x)) -> sent(check(x))
weak:
rest(nil()) -> sent(nil())
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
rest(cons(x,y)) -> sent(y)
top(sent(x)) -> top(check(rest(x)))
check(cons(x,y)) -> cons(x,y)
check(rest(x)) -> rest(check(x))
Matrix Interpretation Processor:
dimension: 4
max_matrix:
[1 1 1 1]
[0 0 1 1]
[0 0 1 1]
[0 0 0 0]
interpretation:
[1 0 0 0] [1 0 1 0] [1]
[0 0 1 0] [0 0 0 1] [0]
[cons](x0, x1) = [0 0 1 0]x0 + [0 0 1 1]x1 + [0]
[0 0 0 0] [0 0 0 0] [0],
[0]
[0]
[nil] = [0]
[1],
[1 0 1 0]
[0 0 1 0]
[check](x0) = [0 0 1 0]x0
[0 0 0 0] ,
[1 0 0 1] [0]
[0 0 1 1] [1]
[rest](x0) = [0 0 1 0]x0 + [1]
[0 0 0 0] [0],
[1 1 0 0] [0]
[0 0 1 0] [1]
[top](x0) = [0 0 1 0]x0 + [0]
[0 0 0 0] [0],
[1 0 1 0] [1]
[0 0 1 1] [1]
[sent](x0) = [0 0 1 0]x0 + [1]
[0 0 0 0] [0]
orientation:
[1 0 2 0] [2] [1 0 2 0] [1]
[0 0 1 0] [1] [0 0 1 0] [1]
check(sent(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = sent(check(x))
[0 0 0 0] [0] [0 0 0 0] [0]
[1] [1]
[2] [2]
rest(nil()) = [1] >= [1] = sent(nil())
[0] [0]
[1 0 1 0] [1 0 2 1] [1] [1 0 1 0] [1 0 1 0] [1]
[0 0 1 0] [0 0 1 1] [0] [0 0 1 0] [0 0 0 1] [0]
check(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [0] >= [0 0 1 0]x + [0 0 1 1]y + [0] = cons(check(x),y)
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0]
[1 0 1 0] [1 0 2 1] [1] [1 0 0 0] [1 0 2 0] [1]
[0 0 1 0] [0 0 1 1] [0] [0 0 1 0] [0 0 0 0] [0]
check(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [0] >= [0 0 1 0]x + [0 0 1 0]y + [0] = cons(x,check(y))
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0]
[1 0 0 0] [1 0 1 0] [1] [1 0 1 0] [1]
[0 0 1 0] [0 0 1 1] [1] [0 0 1 1] [1]
rest(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [1] >= [0 0 1 0]y + [1] = sent(y)
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0]
[1 0 2 1] [2] [1 0 2 1] [2]
[0 0 1 0] [2] [0 0 1 0] [2]
top(sent(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = top(check(rest(x)))
[0 0 0 0] [0] [0 0 0 0] [0]
[1 0 1 0] [1 0 2 1] [1] [1 0 0 0] [1 0 1 0] [1]
[0 0 1 0] [0 0 1 1] [0] [0 0 1 0] [0 0 0 1] [0]
check(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [0] >= [0 0 1 0]x + [0 0 1 1]y + [0] = cons(x,y)
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0]
[1 0 1 1] [1] [1 0 1 0] [0]
[0 0 1 0] [1] [0 0 1 0] [1]
check(rest(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = rest(check(x))
[0 0 0 0] [0] [0 0 0 0] [0]
problem:
strict:
weak:
check(sent(x)) -> sent(check(x))
rest(nil()) -> sent(nil())
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
rest(cons(x,y)) -> sent(y)
top(sent(x)) -> top(check(rest(x)))
check(cons(x,y)) -> cons(x,y)
check(rest(x)) -> rest(check(x))
Qed
strict:
check(rest(x)) -> rest(check(x))
weak:
check(sent(x)) -> sent(check(x))
rest(nil()) -> sent(nil())
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
rest(cons(x,y)) -> sent(y)
top(sent(x)) -> top(check(rest(x)))
check(cons(x,y)) -> cons(x,y)
Matrix Interpretation Processor:
dimension: 4
max_matrix:
[1 1 1 1]
[0 0 1 1]
[0 0 1 1]
[0 0 0 0]
interpretation:
[1 0 0 0] [1 0 1 0] [1]
[0 0 0 0] [0 0 1 0] [0]
[cons](x0, x1) = [0 0 1 0]x0 + [0 0 1 1]x1 + [0]
[0 0 0 0] [0 0 0 0] [0],
[0]
[0]
[nil] = [0]
[1],
[1 0 1 0]
[0 0 1 0]
[check](x0) = [0 0 1 0]x0
[0 0 0 0] ,
[1 0 0 1] [0]
[0 0 1 1] [1]
[rest](x0) = [0 0 1 0]x0 + [1]
[0 0 0 0] [0],
[1 1 0 0]
[0 0 0 0]
[top](x0) = [0 0 0 0]x0
[0 0 0 0] ,
[1 0 1 0] [1]
[0 0 1 1] [1]
[sent](x0) = [0 0 1 0]x0 + [1]
[0 0 0 0] [0]
orientation:
[1 0 1 1] [1] [1 0 1 0] [0]
[0 0 1 0] [1] [0 0 1 0] [1]
check(rest(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = rest(check(x))
[0 0 0 0] [0] [0 0 0 0] [0]
[1 0 2 0] [2] [1 0 2 0] [1]
[0 0 1 0] [1] [0 0 1 0] [1]
check(sent(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = sent(check(x))
[0 0 0 0] [0] [0 0 0 0] [0]
[1] [1]
[2] [2]
rest(nil()) = [1] >= [1] = sent(nil())
[0] [0]
[1 0 1 0] [1 0 2 1] [1] [1 0 1 0] [1 0 1 0] [1]
[0 0 1 0] [0 0 1 1] [0] [0 0 0 0] [0 0 1 0] [0]
check(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [0] >= [0 0 1 0]x + [0 0 1 1]y + [0] = cons(check(x),y)
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0]
[1 0 1 0] [1 0 2 1] [1] [1 0 0 0] [1 0 2 0] [1]
[0 0 1 0] [0 0 1 1] [0] [0 0 0 0] [0 0 1 0] [0]
check(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [0] >= [0 0 1 0]x + [0 0 1 0]y + [0] = cons(x,check(y))
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0]
[1 0 0 0] [1 0 1 0] [1] [1 0 1 0] [1]
[0 0 1 0] [0 0 1 1] [1] [0 0 1 1] [1]
rest(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [1] >= [0 0 1 0]y + [1] = sent(y)
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0]
[1 0 2 1] [2] [1 0 2 1] [2]
[0 0 0 0] [0] [0 0 0 0] [0]
top(sent(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = top(check(rest(x)))
[0 0 0 0] [0] [0 0 0 0] [0]
[1 0 1 0] [1 0 2 1] [1] [1 0 0 0] [1 0 1 0] [1]
[0 0 1 0] [0 0 1 1] [0] [0 0 0 0] [0 0 1 0] [0]
check(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [0] >= [0 0 1 0]x + [0 0 1 1]y + [0] = cons(x,y)
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0]
problem:
strict:
weak:
check(rest(x)) -> rest(check(x))
check(sent(x)) -> sent(check(x))
rest(nil()) -> sent(nil())
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
rest(cons(x,y)) -> sent(y)
top(sent(x)) -> top(check(rest(x)))
check(cons(x,y)) -> cons(x,y)
Qed
strict:
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
weak:
rest(nil()) -> sent(nil())
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
rest(cons(x,y)) -> sent(y)
top(sent(x)) -> top(check(rest(x)))
check(cons(x,y)) -> cons(x,y)
Matrix Interpretation Processor:
dimension: 4
max_matrix:
[1 1 1 1]
[0 0 1 1]
[0 0 1 1]
[0 0 0 0]
interpretation:
[1 0 0 0] [1 0 1 1]
[0 0 0 0] [0 0 0 0]
[cons](x0, x1) = [0 0 0 0]x0 + [0 0 1 1]x1
[0 0 0 0] [0 0 0 0] ,
[0]
[0]
[nil] = [0]
[1],
[1 0 0 0]
[0 0 1 0]
[check](x0) = [0 0 1 0]x0
[0 0 0 0] ,
[1 0 0 1]
[0 0 1 1]
[rest](x0) = [0 0 1 0]x0
[0 0 0 0] ,
[1 1 0 0] [0]
[0 0 0 0] [0]
[top](x0) = [0 0 0 0]x0 + [1]
[0 0 0 0] [0],
[1 0 1 0]
[0 0 0 1]
[sent](x0) = [0 0 0 0]x0
[0 0 0 0]
orientation:
[1] [0]
[1] [1]
rest(nil()) = [0] >= [0] = sent(nil())
[0] [0]
[1 0 0 0] [1 0 1 1] [1 0 0 0] [1 0 1 1]
[0 0 0 0] [0 0 1 1] [0 0 0 0] [0 0 0 0]
check(cons(x,y)) = [0 0 0 0]x + [0 0 1 1]y >= [0 0 0 0]x + [0 0 1 1]y = cons(check(x),y)
[0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0]
[1 0 0 0] [1 0 1 1] [1 0 0 0] [1 0 1 0]
[0 0 0 0] [0 0 1 1] [0 0 0 0] [0 0 0 0]
check(cons(x,y)) = [0 0 0 0]x + [0 0 1 1]y >= [0 0 0 0]x + [0 0 1 0]y = cons(x,check(y))
[0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0]
[1 0 0 0] [1 0 1 1] [1 0 1 0]
[0 0 0 0] [0 0 1 1] [0 0 0 1]
rest(cons(x,y)) = [0 0 0 0]x + [0 0 1 1]y >= [0 0 0 0]y = sent(y)
[0 0 0 0] [0 0 0 0] [0 0 0 0]
[1 0 1 1] [0] [1 0 1 1] [0]
[0 0 0 0] [0] [0 0 0 0] [0]
top(sent(x)) = [0 0 0 0]x + [1] >= [0 0 0 0]x + [1] = top(check(rest(x)))
[0 0 0 0] [0] [0 0 0 0] [0]
[1 0 0 0] [1 0 1 1] [1 0 0 0] [1 0 1 1]
[0 0 0 0] [0 0 1 1] [0 0 0 0] [0 0 0 0]
check(cons(x,y)) = [0 0 0 0]x + [0 0 1 1]y >= [0 0 0 0]x + [0 0 1 1]y = cons(x,y)
[0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0]
[1 0 1 0] [1 0 1 0]
[0 0 0 0] [0 0 0 0]
check(sent(x)) = [0 0 0 0]x >= [0 0 0 0]x = sent(check(x))
[0 0 0 0] [0 0 0 0]
[1 0 0 1] [1 0 0 0]
[0 0 1 0] [0 0 1 0]
check(rest(x)) = [0 0 1 0]x >= [0 0 1 0]x = rest(check(x))
[0 0 0 0] [0 0 0 0]
problem:
strict:
weak:
rest(nil()) -> sent(nil())
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
rest(cons(x,y)) -> sent(y)
top(sent(x)) -> top(check(rest(x)))
check(cons(x,y)) -> cons(x,y)
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
Qed
strict:
rest(nil()) -> sent(nil())
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
check(cons(x,y)) -> cons(check(x),y)
weak:
check(cons(x,y)) -> cons(x,check(y))
rest(cons(x,y)) -> sent(y)
top(sent(x)) -> top(check(rest(x)))
check(cons(x,y)) -> cons(x,y)
Matrix Interpretation Processor:
dimension: 3
max_matrix:
[1 0 1]
[0 0 0]
[0 0 1]
interpretation:
[1 0 0] [1 0 1] [0]
[cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0]
[0 0 1] [0 0 1] [1],
[1]
[nil] = [0]
[0],
[1 0 1] [0]
[check](x0) = [0 0 0]x0 + [1]
[0 0 1] [0],
[1 0 0] [0]
[rest](x0) = [0 0 0]x0 + [1]
[0 0 1] [0],
[1 0 0]
[top](x0) = [0 0 0]x0
[0 0 1] ,
[1 0 1] [0]
[sent](x0) = [0 0 0]x0 + [1]
[0 0 1] [0]
orientation:
[1 0 1] [1 0 2] [1] [1 0 0] [1 0 2] [0]
check(cons(x,y)) = [0 0 0]x + [0 0 0]y + [1] >= [0 0 0]x + [0 0 0]y + [0] = cons(x,check(y))
[0 0 1] [0 0 1] [1] [0 0 1] [0 0 1] [1]
[1 0 0] [1 0 1] [0] [1 0 1] [0]
rest(cons(x,y)) = [0 0 0]x + [0 0 0]y + [1] >= [0 0 0]y + [1] = sent(y)
[0 0 1] [0 0 1] [1] [0 0 1] [0]
[1 0 1] [1 0 1]
top(sent(x)) = [0 0 0]x >= [0 0 0]x = top(check(rest(x)))
[0 0 1] [0 0 1]
[1 0 1] [1 0 2] [1] [1 0 0] [1 0 1] [0]
check(cons(x,y)) = [0 0 0]x + [0 0 0]y + [1] >= [0 0 0]x + [0 0 0]y + [0] = cons(x,y)
[0 0 1] [0 0 1] [1] [0 0 1] [0 0 1] [1]
[1] [1]
rest(nil()) = [1] >= [1] = sent(nil())
[0] [0]
[1 0 2] [0] [1 0 2] [0]
check(sent(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = sent(check(x))
[0 0 1] [0] [0 0 1] [0]
[1 0 1] [0] [1 0 1] [0]
check(rest(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = rest(check(x))
[0 0 1] [0] [0 0 1] [0]
[1 0 1] [1 0 2] [1] [1 0 1] [1 0 1] [0]
check(cons(x,y)) = [0 0 0]x + [0 0 0]y + [1] >= [0 0 0]x + [0 0 0]y + [0] = cons(check(x),y)
[0 0 1] [0 0 1] [1] [0 0 1] [0 0 1] [1]
problem:
strict:
weak:
check(cons(x,y)) -> cons(x,check(y))
rest(cons(x,y)) -> sent(y)
top(sent(x)) -> top(check(rest(x)))
check(cons(x,y)) -> cons(x,y)
rest(nil()) -> sent(nil())
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
check(cons(x,y)) -> cons(check(x),y)
Qed